\begin{tabbing}
d{-}world{-}state($D$;$i$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=:d{-}m($D$; $i$).(timed)state\+
\\[0ex]$\times$ (:Action(d{-}decl($D$;$i$))
\\[0ex]$\times$ (\{$m$:d{-}m($D$; $i$).Msg$\mid$ source(mlnk($m$)) = $i$ $\in$ Id\}  List))
\-
\end{tabbing}